$\forall$${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), ${\it upd}$:update{-}spec(${\it ds}$; ${\it da}$).
\\[0ex]update{-}spec{-}decl(${\it upd}$; ${\it ds}$) $\in$ prop\{i:l\}